Nuprl Lemma : comb_for_ifthenelse_wf
4,23
postcript
pdf
(
b
,
A
,
p
,
q
,
z
. if
b
p
else
q
fi)
(
A
:Type
A
A
True
A
)
latex
Definitions
,
True
,
t
T
,
x
:
A
.
B
(
x
)
,
T
Lemmas
ifthenelse
wf
,
squash
wf
,
true
wf
,
bool
wf
origin
b,A,p,q,z. if b
p else q fi) 
(A:TypeAA
TrueA) b,A,p,q,z. if b p else q fi) (A:TypeAATrueA) T
x:A. B(x)T